/*
 * Kodkod -- Copyright (c) 2005-present, Emina Torlak
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */
package kodkod.ast;

import kodkod.ast.operator.Multiplicity;
import kodkod.ast.visitor.ReturnVisitor;
import kodkod.ast.visitor.VoidVisitor;

/**
 * Represents a variable in a {@link QuantifiedFormula quantified formula}, a
 * {@link Comprehension comprehension expression}, or a {@link SumExpression sum
 * expression}. Two variables are the same if and only if they refer to the same
 * object. That is, v1.eauls(v2) <=> v1 == v2. Each variable has a name, which
 * is basically a comment for the purpose of printing, viewing, etc. The name
 * has no meaning otherwise. The arity of a variable specifies the arity of
 * expressions over which the variable can range.
 *
 * @specfield name: String
 * @specfield arity: int
 * @invariant no children
 * @author Emina Torlak
 */
public final class Variable extends LeafExpression {

    /**
     * Constructs a variable with the specified name and arity 1.
     *
     * @ensures this.name' = name && this.arity' = 1
     */
    private Variable(String name) {
        super(name, 1);
    }

    /**
     * Constructs a variable with the specified name and arity.
     *
     * @ensures this.name' = name && this.arity' = arity
     */
    private Variable(String name, int arity) {
        super(name, arity);
    }

    /**
     * Returns a new variable with the specified name and arity 1.
     *
     * @ensures this.name' = name && this.arity' = 1
     */
    public static Variable unary(String name) {
        return new Variable(name);
    }

    /**
     * Returns a new variable with the specified name and arity.
     *
     * @ensures this.name' = name && this.arity' = arity
     * @throws IllegalArgumentException arity < 1
     */
    public static Variable nary(String name, int arity) {
        return new Variable(name, arity);
    }

    /**
     * Returns the declaration that constrains this variable to be bound to at most
     * one element of the given expression: 'this: lone expr'.
     *
     * @return {d: Decl | d.variable = this && d.multiplicity = LONE && d.expression
     *         = expr }
     * @throws NullPointerException expr = null
     * @throws IllegalArgumentException this.arity != expr.arity || expr.arity != 1
     */
    public Decl loneOf(Expression expr) {
        return new Decl(this, Multiplicity.LONE, expr);
    }

    /**
     * Returns the declaration that constrains this variable to be bound to exactly
     * one element of the given expression: 'this: one expr'.
     *
     * @return {d: Decl | d.variable = this && d.multiplicity = ONE && d.expression
     *         = expr }
     * @throws NullPointerException expr = null
     * @throws IllegalArgumentException this.arity != expr.arity || expr.arity != 1
     */
    public Decl oneOf(Expression expr) {
        return new Decl(this, Multiplicity.ONE, expr);
    }

    /**
     * Returns the declaration that constrains this variable to be bound to at least
     * one element of the given expression: 'this: some expr'.
     *
     * @return {d: Decl | d.variable = this && d.multiplicity = SOME && d.expression
     *         = expr }
     * @throws NullPointerException expr = null
     * @throws IllegalArgumentException this.arity != expr.arity || expr.arity != 1
     */
    public Decl someOf(Expression expr) {
        return new Decl(this, Multiplicity.SOME, expr);
    }

    /**
     * Returns the declaration that constrains this variable to be bound to a subset
     * of the elements in the given expression: 'this: set expr'.
     *
     * @return {d: Decl | d.variable = this && d.multiplicity = SET && d.expression
     *         = expr }
     * @throws NullPointerException expr = null
     * @throws IllegalArgumentException this.arity != expr.arity
     */
    public Decl setOf(Expression expr) {
        return new Decl(this, Multiplicity.SET, expr);
    }

    /**
     * Returns the declaration that constrains this variable to be bound to the
     * specified number of the elements in the given expression: 'this: mult expr'.
     *
     * @return {d: Decl | d.variable = this && d.multiplicity = mult && d.expression
     *         = expr }
     * @throws NullPointerException expression = null || mult = null
     * @throws IllegalArgumentException mult = NO
     * @throws IllegalArgumentException mult in ONE + LONE + SOME && expr.arity != 1
     * @throws IllegalArgumentException this.arity != expr.arity
     */
    public Decl declare(Multiplicity mult, Expression expr) {
        return new Decl(this, mult, expr);
    }

    /**
     * {@inheritDoc}
     *
     * @see kodkod.ast.Expression#accept(kodkod.ast.visitor.ReturnVisitor)
     */
    @Override
    public <E, F, D, I> E accept(ReturnVisitor<E,F,D,I> visitor) {
        return visitor.visit(this);
    }

    /**
     * {@inheritDoc}
     *
     * @see kodkod.ast.Node#accept(kodkod.ast.visitor.VoidVisitor)
     */
    @Override
    public void accept(VoidVisitor visitor) {
        visitor.visit(this);
    }

}
